r:RngSig. r+gp  GrpSig 

latex

Up	rings 1
Definitions of Statement	r+gp
Definitions	r+gp, GrpSig, t  T, x:A. B(x)
Lemmas	rng sig wf, bool wf, rng minus wf, rng zero wf, rng plus wf, rng le wf, rng eq wf, rng car wf